1) Field of the Invention
The present invention relates to a logic verification device, a logic verification method, a logic verification program, and a recording medium used to verify the logic of a hardware module such as an LSI (large-scale integration) to be verified.
2) Description of the Related Art
In designing a hardware module such as an LSI, there is conventionally a demand to shorten the design period to improve work efficiency. On the other hand, a verification work to verify whether the hardware module operates correctly is essential. Particularly, in order to maintain high quality, the verification work is important for a large-scale and highly functional hardware module requiring high speed and low power consumption.
In general, this hardware module has a plurality of input/output terminals, and their signals change for each clock cycle. A pattern of the signal change (input/output sequence) is determined according to a specification, and an optional signal cannot be obtained at an optional time. This signal change is explained below based on a hardware module.
FIG. 10 is a block diagram of one example of a general hardware module of which logic is to be verified. In FIG. 10, a hardware module M includes a clock terminal P1 that inputs a clock signal clk, a command input terminal P2 that inputs a command signal cmd, a request input terminal P3 that inputs a request signal req, an acknowledge output terminal P4 that outputs an acknowledge signal ack, and a data input/output terminal P5 that inputs/outputs a 32-bit data signal dat.
According to the specification of this hardware module M, only two patterns of a read operation and a write operation are permitted. FIG. 11 is a waveform diagram of the read operation of the hardware module M, at which operation, the data signal dat (output data outD in FIG. 11) is read. FIG. 12 is a waveform diagram of the write operation of the hardware module M, at which operation, the data signal dat (input data inD in FIG. 12) is written.
“Input constraints” express constraints that the input signal of the read operation shown in FIG. 11 and the input signal of the write operation shown in FIG. 12 must satisfy respectively. The following two input constraints are provided for the hardware module.
(1) Input Constraint of the Read Operation
When the input value of the command signal cmd is “0”, when the input value of the request signal req is “1”, and also when the output value of the acknowledge signal ack is “0”, then the input value of the command signal cmd must be kept at “0” and the input value of the request signal req must be kept at “1” in the next cycle.
(2) Input Constraint of the Write Operation
When the input value of the command signal cmd is “1”, when the input value of the request signal req is “1”, and also when the output value of the acknowledge signal ack is “0”, then the input value of the command signal cmd must be kept at “0” and the input value of the request signal req must be kept at “1” in the next cycle. The input value of data signal dat must also be kept at a same value.
The above input constraints (1) and (2) are essential information to verify the logic. The logic verification is a work to confirm that the hardware module M operates correctly even when the value of the signal input to the input terminal changes within a range of values that satisfy the input constraints. On the other hand, the operation to an input that does not satisfy the input constraint has no meaning of verification.
Violation of the input constraints made by the hardware module M shown in FIG. 10 is explained next. FIG. 13 is a waveform diagram of the input constraints violated by the hardware module M. When operation waveforms shown in FIG. 13 are observed, the hardware module M shown in FIG. 10 has violated the input constraint (2).
Therefore, even when the function of the hardware module M expected for the write operation (for example, to store a value of the data signal dat) is not correctly executed or when the data signal dat taken out in the subsequent read operation does not have an expected value, this must not be determined as a dyslogia of the hardware module M.
In order to correctly verify the above violation of input constraints, verification methods called a formal verification and a constraint-based verification are available, instead of a simple logic simulation. According to these verification methods, it is necessary to prepare a description of an input constraint that a computer can interpret, in addition to a description of a hardware of which logic is to be verified and a description of a verification property expressing the verification content, as inputs to a logic verification tool (see, for example, Non-Patent Literature 1: “A Verification Synergy: Constraint-Based Verification” by Carl Pixley and John Havlicek, Electronic Design Process Workshop, IEEE Computer Society, 2003, and Non-Patent Literature 2: “Creative Assertion and Constraint Methods for Formal Design Verification” by Joseph Richards, Design and Verification Conference and Exhibition (DVCon)).
According to an actual logic verification of the hardware module M, there are several hundred items in the input constraint description shown in the Non-Patent Literatures 1 and 2, and it is not easy to accurately describe every one of these items. Therefore, when there is a description of input constraints, it is possible to automatically and efficiently execute the subsequent logic verification work (see, for example, Non-Patent Literature 3: “Deriving a Simulation Input Generator and a Coverage Metric From a Formal Specification” by Kanna Shimizu and David L. Dill, Design Automation Conference (DAC), 2002, and Non-Patent Literature 4: “Constraint Synthesis for Environment Modeling in Functional Verification” by Jun Yuan, Ken Albin, Adnan Aziz, and Carl Pixley, Design Automation Conference(DAC), 2003).
Exhaustive description of input/output terminals that the hardware module M has, kinds of communications carried out via these input/output terminals, and signal change patterns in each kind of communication is called an interface specification description of the hardware module M.
The interface specification description is useful for the logic verification of a design. The interface specification description can clarify the specification concerning communication procedures, and can share and help the understanding of the specification among designers. A method of generating a logic verification checker and a test pattern from the interface specification description is disclosed in Non-Patent Literature 5 (“A proposal for transaction-level verification with Component Wrapper Language” by Koji Ara and Kei Suzuki, Design Automation and Test in Europe (DATE), 2003).
According to the conventional techniques described in the Non-Patent Literatures 1 to 5, however, description of input constraints that a computer can interpret is necessary for the formal verification and the constraint-based verification. Therefore, concerning a newly designed hardware module, an engineer who understands this hardware module manually describes the input constraint, which is troublesome.
Each time when the specification is changed or corrected, the engineer must manually describe the change or the correction, which is also troublesome. The dependence on the manual work by the engineer as described above takes time for the verification work and also for the design work.
The dependence on the manual work by the engineer may lead to a leakage or an error in the prepared description of input constraints. As a result, the logic verification cannot be carried out correctly, the precision of the logic verification is lowered, and the production yield is lowered.